I am a researcher in computer science at Inria, since January 2015, in the PARTOUT team.

My research topic. I study higher-order computations, the approach to computation where the inputs and the outputs of a program are not simply numbers, strings, or compound data types but also programs themselves. I mainly study the lambda calculus, the mathematical core formalism for higher-order computations, using a combination of tools from logic, graphical syntaxes, rewriting theory, computational complexity, denotational semantics, concurrency, and implementations of programming languages.

The main fields of application are functional programming languages such as OCaml or Haskell, but functional features are nowadays also found in mainstream languages such as Java or Python, and proof assistants such as Lean, Rocq, or Agda. In addition, the lambda-calculus is also of interest for its mathematical connections to proof theory and category theory.

Bird's Eye View. My research work is an attempt to connect different tools and perspectives in the study of the lambda calculus. There are two main recurrent and correlated themes in my work, one of an internal nature and one of an external nature:

• Internal: connecting the classical mathematical theory of the lambda calculus with the practice of the implementations of functional languages, by building a mathematical theory of sharing, the crucial ingredient for efficiency;

• External: reconciling the schism between the lambda calculus and computational complexity, by studying reasonable cost models for time and space in the lambda calculus.

Both topics have been reshaped by the results that I have obtained in various collaborations. In particular, I was involved in the solution of three long-standing open problems:

1. Sharing: finding the canonical lambda calculus with first-class sharing. The lambda calculus can be enriched with sharing (or explicit substitutions) in many different ways. Since the 1990s many calculi have been proposed, usually with complex theories and unable to preserve the properties of the lambda calculus. In collaboration with Delia Kesner, I introduced the linear substitution calculus, which is simpler than all previously calculi, preserves the properties of the lambda calculus, and has some properties that the lambda calculus does not (for instance, postponement of garbage collection and confluence in the weak case). See papers [C5,C6,C10,C22] below.

2. Time: finding the first reasonable time cost model for the lambda calculus. In collaboration with Ugo Dal Lago, I proved that the lambda calculus is a reasonable computational model for time, i.e. that it is polynomially related to Turing machines, see paper [J3] below. Our proof solved a long-standing open problem, and in an unexpected way. The lambda calculus was indeed suspected to be unreasonable because of a negative result due to Asperti and Mairson (in POPL '98). This is my most important contribution, and a major development in the theory of lambda calculus.

3. Logarithmic space: finding the first reasonable space cost model for the lambda calculus accounting for logarithmic space. Logarithmic space has to be measured via an abstract machine, and it was conjectured that one had to use token-based machines, because environment-based ones could not be space reasonable (that is, equivalent to Turing machines). In collaboration with Ugo Dal Lago and Gabriele Vanoni, we first refuted the conjecture about token-machines in paper [C32] below, and then in [C36] we introduced an environment-based machine that, against expectations, provides the first reasonable cost model for logarithmic space.

Beyond these results, I develop(ed) fresh perspectives and in-depth studies of the following topics:

• Call-by-value/need: for applications, the call-by-value and call-by-need lambda calculi are prefered to the ordinary (or call-by-name) one, because they are 'more efficient' but their foundations are much less developed. Since 2012, I am building a theory of call-by-value from many different points of view (logical, operational, denotational, implementations, cost models, rewriting, equational theories), laid out in [C4, C12-14, C17-18, C20, C23-25, C33, C38, C41, C43-44, C46, C47, C51, C52, J2, J4-5]; see the intro of [C23] for an introductive speech. My main co-author on the topic is Giulio Guerrieri. In parallel, I have also been doing a similar study of call-by-need in [C13, C19-20, C24, C34, C44, C49].

• Abstract machines: in many joint works [C13, C14-16, C18-19, C25-26, C29, C31-33, C36, C40, C45, C49, C51-52, J5, J8], I outlined a new theory of abstract machines for the lambda calculus based on complexity analyses of the many choices involved in the design of machines. The analyses led to the introduction of new, faster machines and implementation techniques. This line of work started in 2014 in [C13]. My main co-author on the topic is Claudio Sacerdoti Coen.

• Multi types: intersection types are a standard tool for the study of the lambda calculus, mediating between operational and denotational aspects. In a seminal but hard to grasp work, De Carvalho showed that a variant of intersection types - sometimes called multi types - can be used for quantitative analyses. I spent much effort in refining his work, building an extended theory in [C21, C23-24, C31-32, C37-38, C41-44, C48, J6]. This line of research started in 2018 in [C21], as a collaboration with Delia Kesner, who in parallel provided many further and complementary works on the topic. The introduction of [C37] is a good introductive speech.

• Contextual equivalence: the reference notion of program equivalence is contextual equivalence. In various works [C38, C43-44, C48, C50, U3], I have been studying contextual equivalence in lambda calculi, often with respect to a cost-based point of view. The main outcome has been the introduction of interaction equivalence in [C48], a quantitative refinement of contextual equivalence. My main co-author on the topic is Adrienne Lancelot.

• Additionally: I have also worked repeatedly on linear logic [C8-9, C22, C35, C45, J2, J7], rewriting techniques for lambda calculi [C2-3, C6, C10, C27, C30, C35, J1, J7], and the formalization of the theory of lambda calculus in proof assistants [C7, C39, C50].

My HDR thesis is an overview of 15 years of research (2011-25) that might be a good introduction to my work.

E-mail: "givenname"."familyname" at inria.fr